add tests for conseq equiv phoare

* reduce in t_hF_or_bhF_or_eF
* add reduction in call tactic

…a more robust pattern

All code that relates to module replacement is now usused and has
been removed.

This commit makes the warning flags now explicit for the dev/ci
environments and use the same set of warning flags for both of them.
This will allow us to catch more warnings in the CI.

For the release environment, we now use the default set of flags.

As a side effect, this commit fixes the pretty printing of local
variables (the actual code was not using the printing environment
anymore to get the display name)

Currently, if the top-assumption is not an hypothesis, we
let an low-tactic error message do escape. We now write a
proper error message before this happens.

Check modules in types + properly classify declared modules as declared

ECO version is now 4.

The trace field is optional. The -trace command line option triggers
the trace recording in the generated .eco file.

The second goal generated from byehoare is unsound, in
which the procedure arguments are bound in a free memory.

This is a small bug introduced in #789 . We need to use
the default memory (hr) of the program.

This logic is deliberately slightly less expressive than the one it
replaces, which does not hinder usability in any cryptographic context,
with the hope that it is simpler to maintain and verify.

The spelling 'instanciate' is only acknowledged in the Wiktionary, while
all other dictionaries prefer the spelling with a 't'.

ex.: https://dictionary.cambridge.org/dictionary/english/instantiate

…ports

fix: perform positivity check in type arguments of type constructors
test: add a simple test file for positivity checking.